perm filename ASSOC[EKL,SYS]1 blob
sn#818986 filedate 1986-06-13 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00017 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00003 00002 functions as association lists
C00007 00003 facts about alists
C00012 00004 * proofs
C00023 00005 lemma 3
C00027 00006 lemma 4
C00031 00007 theorem 1 (i) lemma range compose, part 1
C00035 00008 theorem 1 (i) lemma range compose, part 2
C00040 00009 theorem 1 (i), conclusion.
C00044 00010 theorem 1 (ii)
C00046 00011 samemap left
C00049 00012 theorem 2 (i) (permutp idalistp)
C00059 00013 theorem 2 (ii) (idalistp right)
C00070 00014 theorem 2 (iii) (idalistp left)
C00073 00015 a lemma: the range of a permutation contains only atoms
C00075 00016 theorem 3 (i)
C00078 00017 theorem 3 (ii) and (iii)
C00089 ENDMK
C⊗;
;functions as association lists
(wipe-out)
(get-proofs appl)
(proof assoc)
(decl (compalist) (infixname: |∞|) (type: |ground⊗ground→ground|)
(syntype: constant) (bindingpower: 930))
(defax compalist |∀alist1 alist2 xa y.nil∞alist2=nil∧
((xa.y).alist1)∞alist2=(xa.appalist(y,alist2)).(alist1∞alist2)|)
(label compalistdef)
(decl invalist (type: GROUND→GROUND))
(defax invalist |∀alist xa y.invalist nil=nil∧
invalist((xa.y).alist)=(y.xa).invalist alist|)
(label invalistdef)
(decl idalistp (type: GROUND→TRUTHVAL))
(defax idalistp |∀alist xa y.idalistp(nil)∧
(idalistp((xa.y).alist)≡xa=y∧idalistp alist)|)
(label idalistpdef)
;facts about alists
(proof alistfacts)
;check the sorts
(axiom |∀alist alist1.alistp(alist ∞ alist1)|)
(label compalistsort)(label simpinfo)
(axiom |∀alist.allp(λx.atom x,range(alist))⊃alistp invalist(alist)|)
(label invalistsort)
;facts about composition of functions
;five lemmata
(axiom |∀alist alist1 x.member(x,dom(alist))⊃
appalist(x,alist∞alist1)=appalist(appalist(x,alist),alist1)|)
(label alist_lemma1)(label app_compalist)
(axiom |∀alist alist1.dom(alist∞alist1)=dom(alist)|)
(label alist_lemma2)(label dom_compalist)
(axiom |∀alist x.member(x,dom alist)⊃
(∃y.member(y,range alist)∧appalist(x,alist)=y)|)
(label alist_lemma3) (label nonempty_range)
(axiom |∀alist z.uniqueness dom(alist)∧member(z,range alist)⊃
(∃x.member(x,dom alist)∧appalist(x,alist)=z)|)
(label alist_lemma4) (label nonempty_domain)
(axiom |∀alist alist1 za z.¬member(za,range(alist))⊃
alist∞((za.z).alist1)=alist∞alist1|)
(label compalist_lemma)
;theorem 1: composition of permutations is a permutation
;PERMUTP(ALIST)∧PERMUTP(ALIST1)∧MKLSET(DOM(ALIST))=MKLSET(DOM(ALIST1))⊃
;PERMUTP(ALIST∞ALIST1)
;the steps in the proof of Theorem 1 are the following
;lemma range compose
(axiom
|∀alist alist1.permutp(alist)∧permutp(alist1)∧
mklset(dom(alist))=mklset(dom(alist1))⊃
mklset(range(alist∞alist1))⊂mklset(range(alist1))|)
(label range_compose)
(axiom
|∀alist alist1.permutp(alist)∧permutp(alist1)∧
mklset(dom(alist))=mklset(dom(alist1))⊃
mklset(range(alist1))⊂mklset(range(alist∞alist1))|)
(label range_compose)
;composition is well defined for equivalence classes
(axiom |∀alist alist1 alist2.samemap(alist1,alist2)⊃
alist∞alist1=alist∞alist2|)
(label samamap_right)
(axiom |∀alist1 alist2.samemap(alist1,alist2)⊃
samemap(alist1∞alist,alist2∞alist)|)
(label samamap_left)
;facts about the identity function
(axiom |∀alist y.idalistp(alist)∧member(y,dom alist)⊃appalist(y,alist)=y|)
(label idalistp_main)
;theorem 2 (i)
;∀ALIST.FUNCTP(ALIST)∧IDALISTP(ALIST)⊃PERMUTP(ALIST)
;theorem 2 (ii)
;IDALISTP(ALIST1)⊃
;(∀ALIST.MKLSET(RANGE(ALIST))⊂MKLSET(DOM(ALIST1))⊃ALIST∞ALIST1=ALIST)
;theorem 2 (iii)
;IDALISTP(ALISTID)∧MKLSET(DOM(ALISTID))=MKLSET(DOM(ALIST))⊃
;SAMEMAP(ALISTID∞ALIST,ALIST)
;facts about inversion of functions
(axiom |∀alist.allp(λx.atom x,range(alist))⊃dom(invalist(alist))=range(alist)|)
(label dom_invalist)
(axiom |∀alist.allp(λx.atom x,range(alist))⊃range(invalist(alist))=dom(alist)|)
(label range_invalist)
(axiom |∀alist.mklset(dom(alist))=mklset(range(alist))⊃
allp(λx.atom x,range(alist))|)
(label atomrange)
;theorem 3 (i)
;∀ALIST.ALLP(λX.ATOM X,RANGE(ALIST))∧INJECTP(ALIST)⊃
; IDALISTP(ALIST∞INVALIST(ALIST))
;theorem 3 (ii)
;∀ALIST.ALLP(λX.ATOM X,RANGE(ALIST))∧INJECTP(ALIST)⊃
; IDALISTP(INVALIST(ALIST)∞ALIST)
;theorem 3 (iii)
;PERMUTP(ALIST)⊃PERMUTP(INVALIST(ALIST))
(save-proofs assoc)
;* proofs
(wipe-out)
(get-proofs assoc)
(proof alistprop)
;prove sorts
;compalist sort
(unlabel simpinfo compalistsort)
1. (ue (chi |λalist.alistp(alist ∞ alist1)|) alistinduction
(part 1(open compalist)(use appalistsort mode: exact)))
;∀ALIST.ALISTP ALIST∞ALIST1
(label simpinfo compalistsort)
;invalistsort
2. (ue (chi |λalist.allp(λx.atom x,range alist)⊃alistp invalist(alist)|)
alistinduction (open range member invalist)
(use allpfact ue: ((phi.|λx.atom x|)(x.y)(u.|range alist|)) mode: always) )
;∀ALIST.ALLP(λX.ATOM X,RANGE(ALIST))⊃ALISTP INVALIST(ALIST)
;prove facts about composition of functions
;three (of five) lemmata
;lemma 1
3. (ue (chi |λalist.member(x,dom(alist))⊃
appalist(x,alist∞alist1)=appalist(appalist(x,alist),alist1)|)
alistinduction
(part 1(use appalistdef mode: always)
(open dom member compalist assoc))
(use normal mode: always))
;∀ALIST.MEMBER(X,DOM(ALIST))⊃
; APPALIST(X,ALIST∞ALIST1)=APPALIST(APPALIST(ALIST,X),ALIST1)
;lemma 2
4. (ue (chi |λalist.dom(alist∞alist1)=dom(alist)|)
alistinduction
(open compalist dom))
;∀ALIST.DOM(ALIST∞ALIST1)=DOM(ALIST)
;compalist lemma
5. (ue (chi |λalist.¬member(za,range alist)⊃alist∞((za.z).alist1)=alist∞alist1|)
alistinduction
(open member range compalist appalist assoc) (use demorgan mode: always))
;∀ALIST.¬MEMBER(ZA,RANGE(ALIST))⊃ALIST∞((ZA.Z).ALIST1)=ALIST∞ALIST1
;samemap right
6. (ue (chi |λalist.samemap(alist1,alist2)⊃alist∞alist1=alist∞alist2|)
alistinduction
(part 1(use samemap_def1 mode: exact))
(part 1(open compalist samemap)))
;∀ALIST.SAMEMAP(ALIST1,ALIST2)⊃ALIST∞ALIST1=ALIST∞ALIST2
;prove a fact about the identity function
;idalistp_main
7. (ue (chi |λalist.idalistp(alist)∧member(y,dom alist)⊃appalist(y,alist)=y|)
alistinduction
(open idalistp appalist assoc member dom) (use normal mode: always))
;∀ALIST.IDALISTP(ALIST)∧MEMBER(Y,DOM(ALIST))⊃CDR ASSOC(Y,ALIST)=Y
;prove facts about inversion of functions
;dom invalist
8. (ue (chi |λalist.allp(λx.atom x,range alist)⊃dom invalist(alist)=range alist|)
alistinduction (open dom range invalist) (use invalistsort)
(use allpfact ue: ((phi.|λx.atom x|)(x.y)(u.|range alist|)) mode: always) )
;∀ALIST.ALLP(λX.ATOM X,RANGE(ALIST))⊃DOM(INVALIST(ALIST))=RANGE(ALIST)
;range invalist
9. (ue (chi |λalist.allp(λx.atom x,range alist)⊃range invalist(alist)=dom alist|)
alistinduction (open dom range invalist) (use invalistsort)
(use allpfact ue: ((phi.|λx.atom x|)(x.y)(u.|range alist|)) mode: always) )
;∀ALIST.ALLP(λX.ATOM X,RANGE(ALIST))⊃RANGE(INVALIST(ALIST))=DOM(ALIST)
;lemma 3
;should be able to do this in one step
(ue (chi |λalist.member(x,dom alist)⊃
(∃y.member(y,range alist)∧appalist(x,alist)=y)|)
alistinduction
(use excluded_middle ue:
((p.|∃y1.member(y1,range((xa.y).alist))∧appalist(x,(xa.y).alist)=y1|)
(q.|x=xa|)) normal mode: always)
(open dom range member appalist assoc))
;LIST STORAGE CAPACITY EXCEEDED
;BKPT GC-LOSSAGE
(wipe-out)
(get-proofs assoc)
(proof alist_lemma3)
1. (assume |MEMBER(X,DOM(ALIST))⊃
(∃Y1.MEMBER(Y1,RANGE(ALIST))∧CDR ASSOC(X,ALIST)=Y1)|)
(label lem31)
2. (assume |member(x,dom((xa.y).alist))|)
(label lem32)
3. (rw * (open dom member))
;X=XA∨MEMBER(X,DOM(ALIST))
(label lem33)
4. (assume |x=xa|)
5. (trw |∃y1.member(y1,range((xa.y).alist))∧appalist(x,(xa.y).alist)=y1|
(open appalist assoc range member) (use * mode: exact))
;∃Y1.MEMBER(Y1,RANGE((XA.Y).ALIST))∧APPALIST(X,(XA.Y).ALIST)=Y1
(label lem34)
6. (assume |x≠xa|)
(label lem35)
7. (derive |member(x,dom(alist))| (lem33 *))
(label lem36)
8. (define yv |member(yv,range(alist))∧cdr assoc(x,alist)=yv| (lem31 lem36))
(label lem37)
9. (derive |∃y1.member(y1,range((xa.y).alist))∧appalist(x,(xa.y).alist)=y1| *
(open appalist assoc range) (use memberdef lem35 mode: always))
(label lem38)
10. (trw |x=xa∨x≠xa|)
11. (cases * lem34 lem38)
;∃Y1.MEMBER(Y1,RANGE((XA.Y).ALIST))∧APPALIST(X,(XA.Y).ALIST)=Y1
;deps: (LEM31 LEM32)
12. (ci lem32)
;MEMBER(X,DOM((XA.Y).ALIST))⊃
;(∃Y1.MEMBER(Y1,RANGE((XA.Y).ALIST))∧APPALIST(X,(XA.Y).ALIST)=Y1)
;deps: (LEM31)
13. (ci lem31)
14. (ue (chi |λalist.member(x,dom alist)⊃
(∃y.member(y,range alist)∧appalist(x,alist)=y)|)
alistinduction
(use * mode: exact)(part 1#1(open dom member)))
;∀ALIST.MEMBER(X,DOM(ALIST))⊃
; (∃Y.MEMBER(Y,RANGE(ALIST))∧APPALIST(X,ALIST)=Y)
;lemma 4
(wipe-out)
(get-proofs assoc)
(proof alist_lemma4)
1. (assume |uniqueness dom(alist)∧member(z,range alist)⊃
(∃x.member(x,dom alist)∧appalist(x,alist)=z)|)
(label lem41)
2. (assume |uniqueness dom((xa.y).alist)|)
(label lem42)
3. (rw * (open uniqueness dom))
;¬MEMBER(XA,DOM(ALIST))∧UNIQUENESS(DOM(ALIST))
(label lem43)
;deps: (LEM42)
4. (assume |member(z,range((xa.y).alist))|)
(label lem44)
5. (rw * (open range member))
;Z=Y∨MEMBER(Z,RANGE(ALIST))
(label lem45)
;deps: (LEM44)
6. (assume |z=y|)
7. (trw |∃x1.member(x1,dom((xa.y).alist))∧appalist(x1,(xa.y).alist)=z|
(open dom member appalist assoc) (use * mode: exact))
;∃X1.MEMBER(X1,DOM((XA.Y).ALIST))∧APPALIST(X1,(XA.Y).ALIST)=Z
(label lem46)
8. (assume |member(z,range(alist))|)
(label lem47)
9. (define xxv |member(xxv,dom alist)∧appalist(xxv,alist)=z|(lem41 lem43 lem47))
(label lem48)
10. (derive |xxv≠xa| (lem43 lem48))
;deps: (LEM41 LEM42 LEM47)
11. (trw |appalist(xxv,(xa.y).alist)=z| (open appalist assoc)
(use * mode: exact)(use lem48 mode: always direction: reverse))
;APPALIST(XXV,(XA.Y).ALIST)=Z
;deps: (LEM41 LEM42 LEM47)
12. (derive |∃x1.member(x1,dom((xa.y).alist))∧appalist(x1,(xa.y).alist)=z|
(lem48 *) (open dom) (use memberdef mode: always))
(label lem49)
;deps: (LEM41 LEM42 LEM47)
13. (cases lem45 lem46 lem49)
;∃X1.MEMBER(X1,DOM((XA.Y).ALIST))∧APPALIST(X1,(XA.Y).ALIST)=Z
;deps: (LEM41 LEM42 LEM44)
14. (ci (lem42 lem44))
;UNIQUENESS(DOM((XA.Y).ALIST))∧MEMBER(Z,RANGE((XA.Y).ALIST))⊃
;(∃X1.MEMBER(X1,DOM((XA.Y).ALIST))∧APPALIST(X1,(XA.Y).ALIST)=Z)
;deps: (LEM41)
15. (ci lem41)
16. (ue (chi |λalist.uniqueness dom(alist)∧member(z,range alist)⊃
(∃x.member(x,dom alist)∧appalist(x,alist)=z)|)
alistinduction
(part 1#1(open range member))(use * mode: exact))
;∀ALIST.UNIQUENESS(DOM(ALIST))∧MEMBER(Z,RANGE(ALIST))⊃
; (∃X.MEMBER(X,DOM(ALIST))∧APPALIST(X,ALIST)=Z)
;theorem 1 (i); lemma range compose, part 1
(wipe-out)
(get-proofs assoc)
(proof range_compose)
1. (assume |permutp(alist)|)
(label rc1)
2. (rw * (open permutp functp))
;UNIQUENESS(DOM(ALIST))∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))
(label rc2)
3. (assume |mklset dom(alist)=mklset dom(alist1)|)
(label rc3)
4. (assume |member(z,range(alist∞alist1))|)
(label rc4)
;apply lemma 4 and lemma 2
5. (ue ((alist.|alist∞alist1|)(z.z)) alist_lemma4
(use alist_lemma2 rc2 rc4 mode: exact) )
;deps: (RC1 RC4)
;∃X.MEMBER(X,DOM(ALIST))∧APPALIST(X,ALIST∞ALIST1)=Z
6. (define xxvv |member(xxvv,dom alist)∧appalist(xxvv,alist∞alist1)=z| *)
(label rc5)
;deps: (RC1 RC4)
;apply lemma 1
7. (rw * (use alist_lemma1 mode: always))
;MEMBER(XXVV,DOM(ALIST))∧APPALIST(APPALIST(XXVV,ALIST),ALIST1)=Z
(label rc6)
;deps: (RC1 RC4)
;apply lemma 3
8. (define yyvv |member(yyvv,range alist)∧appalist(xxvv,alist)=yyvv|
(alist_lemma3 rc6))
(label rc7)
;deps: (RC1 RC4)
9. (trw |yyvv ε mklset range(alist)| (open mklset epsilon) rc7)
;YYVVεMKLSET(RANGE(ALIST))
;deps: (RC1 RC4)
10. (rw * (use rc2 mode: exact direction: reverse)
(use rc3 mode: exact))
;YYVVεMKLSET(DOM(ALIST1))
;deps: (RC1 RC3 RC4)
11. (rw * (open epsilon mklset))
;MEMBER(YYVV,DOM(ALIST1))
;deps: (RC1 RC3 RC4)
;apply again lemma 3, this time to alist1
12. (define zzvv |member(zzvv,range alist1)∧appalist(yyvv,alist1)=zzvv|
(alist_lemma3 *))
(label rc8)
;deps: (RC1 RC3 RC4)
13. (rw rc6 rc7)
;MEMBER(XXVV,DOM(ALIST))∧APPALIST(YYVV,ALIST1)=Z
;deps: (RC1 RC4)
14. (trw |zzvv=z| * (use rc8 mode: always direction: reverse))
;ZZVV=Z
;deps: (RC1 RC3 RC4)
15. (trw |member(z,range alist1)| rc8 (use * mode: exact direction: reverse))
;MEMBER(Z,RANGE(ALIST1))
;deps: (RC1 RC3 RC4)
16. (ci rc4)
;MEMBER(Z,RANGE(ALIST∞ALIST1))⊃MEMBER(Z,RANGE(ALIST1))
;deps: (RC1 RC3)
17. (trw |mklset range(alist∞alist1)⊂mklset range(alist1)| *
(open mklset inclusion))
;MKLSET(RANGE(ALIST∞ALIST1))⊂MKLSET(RANGE(ALIST1))
;deps: (RC1 RC3)
18. (ci (rc1 rc3))
;PERMUTP(ALIST)∧MKLSET(DOM(ALIST))=MKLSET(DOM(ALIST1))⊃
;MKLSET(RANGE(ALIST∞ALIST1))⊂MKLSET(RANGE(ALIST1))
;theorem 1 (i); lemma range compose, part 2
(proof range_compose2)
1. (assume |permutp(alist)|)
(label rc21)
2. (rw * (open permutp functp))
;UNIQUENESS(DOM(ALIST))∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))
(label rc22)
3. (assume |permutp(alist1)|)
(label rc23)
4. (rw * (open permutp functp))
;UNIQUENESS(DOM(ALIST1))∧MKLSET(DOM(ALIST1))=MKLSET(RANGE(ALIST1))
(label rc24)
5. (assume |mklset dom(alist)=mklset dom(alist1)|)
(label rc25)
6. (assume |member(z,range alist1)|)
(label rc26)
;apply lemma 4
7. (define yv1 |member(yv1,dom alist1)∧appalist(yv1,alist1)=z|
(alist_lemma4 rc24 rc26))
(label rc27)
;deps: (RC23 RC26)
8. (trw |yv1 ε mklset dom(alist1)| * (open epsilon mklset))
;YV1εMKLSET(DOM(ALIST1))
;deps: (RC23 RC26)
9. (rw * (use rc25 mode: exact direction: reverse)
(use rc22 mode: exact))
;YV1εMKLSET(RANGE(ALIST))
;deps: (RC21 RC23 RC25 RC26)
10. (rw * (open epsilon mklset))
;MEMBER(XV1,RANGE(ALIST))
(label rc28)
;deps: (RC21 RC23 RC25 RC26)
;apply again lemma 4, this time to alist
11. (define xv1 |member(xv1,dom alist)∧appalist(xv1,alist)=yv1|
(alist_lemma4 rc22 rc28))
(label rc29)
;deps: (RC21 RC23 RC25 RC26)
;apply lemma 2 and rewrite
12. (trw |member(xv1,dom(alist∞alist1))| * (use alist_lemma2))
;MEMBER(XV1,DOM(ALIST∞ALIST1))
(label rc30)
;deps: (RC21 RC23 RC25 RC26)
13. (trw |appalist(xv1,alist∞alist1)| rc29 rc30
(use alist_lemma1 rc29 rc27 mode: always))
;APPALIST(XV1,ALIST∞ALIST1)=Z
(label rc31)
;deps: (RC21 RC23 RC25 RC26)
;apply lemma 3
14. (ue ((alist.|alist∞alist1|)(x.xv1)) alist_lemma3
(use alist_lemma2 rc22 rc30 mode: always))
;∃Y.MEMBER(Y,RANGE(ALIST∞ALIST1))∧APPALIST(XV1,ALIST∞ALIST1)=Y
;deps: (RC21 RC23 RC25 RC26)
15. (define zv1
|member(zv1,range(alist∞alist1))∧appalist(xv1,alist∞alist1)=zv1| *)
(label rc32)
;deps: (RC21 RC23 RC25 RC26)
16. (trw |zv1=z| rc31 (use * mode: always direction: reverse))
;ZV1=Z
;deps: (RC21 RC23 RC25 RC26)
17. (trw |member(z,range(alist∞alist1))| rc32
(use * mode: exact direction: reverse))
;MEMBER(Z,RANGE(ALIST∞ALIST1))
;deps: (RC21 RC23 RC25 RC26)
18. (ci rc26)
;MEMBER(Z,RANGE(ALIST1))⊃MEMBER(Z,RANGE(ALIST∞ALIST1))
;deps: (RC21 RC23 RC25)
19. (trw |mklset range(alist1)⊂mklset range(alist∞alist1)| *
(open inclusion mklset) )
;MKLSET(RANGE(ALIST1))⊂MKLSET(RANGE(ALIST∞ALIST1))
;deps: (RC21 RC23 RC25)
20. (ci (rc21 rc23 rc25))
;PERMUTP(ALIST)∧PERMUTP(ALIST1)∧MKLSET(DOM(ALIST))=MKLSET(DOM(ALIST1))⊃
;MKLSET(RANGE(ALIST1))⊂MKLSET(RANGE(ALIST∞ALIST1))
;theorem 1 (i), conclusion.
(proof permutp_compalist)
1. (assume |permutp(alist)|)
(label permut_comp1)
2. (assume |permutp(alist1)|)
(label permut_comp2)
3. (assume |mklset(dom(alist))=mklset(dom(alist1))|)
(label permut_comp3)
4. (derive |mklset(range(alist∞alist1))⊂mklset(range(alist1))∧
mklset(range(alist1))⊂mklset(range(alist∞alist1))|
(permut_comp1 permut_comp2 permut_comp3 range_compose))
;deps: (PERMUT_COMP1 PERMUT_COMP2 PERMUT_COMP3)
5. (derive |mklset(range(alist∞alist1))=mklset(range(alist1))|
(* double_inclusion))
;deps: (PERMUT_COMP1 PERMUT_COMP2 PERMUT_COMP3)
(label permut_comp4)
6. (rw permut_comp1 (open permutp functp))
;UNIQUENESS(DOM(ALIST))∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))
(label permut_comp5)
7. (rw permut_comp2 (open permutp))
;FUNCTP(ALIST1)∧MKLSET(DOM(ALIST1))=MKLSET(RANGE(ALIST1))
8. (trw |uniqueness(dom(alist∞alist1))∧
mklset dom(alist∞alist1)=mklset range(alist∞alist1)|
(use alist_lemma2 permut_comp4 mode: exact) permut_comp5
(use * permut_comp3 mode: always direction: reverse))
;UNIQUENESS(DOM(ALIST∞ALIST1))∧
;MKLSET(DOM(ALIST∞ALIST1))=MKLSET(RANGE(ALIST∞ALIST1))
;deps: (PERMUT_COMP1 PERMUT_COMP2 PERMUT_COMP3)
9. (trw |permutp(alist∞alist1)| * (open permutp functp))
;PERMUTP(ALIST∞ALIST1)
;deps: (PERMUT_COMP1 PERMUT_COMP2 PERMUT_COMP3)
10. (ci (permut_comp1 permut_comp2 permut_comp3))
;PERMUTP(ALIST)∧PERMUTP(ALIST1)∧MKLSET(DOM(ALIST))=MKLSET(DOM(ALIST1))⊃
;PERMUTP(ALIST∞ALIST1)
;theorem 1 (ii)
(wipe-out)
(get-proofs assoc)
(proof compalist_associativity)
1. (trw |mklset(range((xa.y).alist))⊂mklset(dom alist1)⊃
member(y,dom alist1)∧mklset range(alist)⊂mklset dom(alist1)|
(open mklset inclusion range member)(use normal mode: always))
;MKLSET(RANGE((XA.Y).ALIST))⊂MKLSET(DOM(ALIST1))⊃
;MEMBER(Y,DOM(ALIST1))∧MKLSET(RANGE(ALIST))⊂MKLSET(DOM(ALIST1))
2. (trw |member(y,dom alist1)∧mklset range(alist)⊂mklset dom(alist1)⊃
mklset(range((xa.y).alist))⊂mklset(dom alist1)| (der)
(open mklset inclusion range member)(use normal mode: always))
3. (derive |mklset(range((xa.y).alist))⊂mklset(dom alist1)≡
member(y,dom alist1)∧mklset range(alist)⊂mklset dom(alist1)| (* -2))
(label helpinduction)
4. (ue (chi |λalist.mklset(range alist)⊂mklset(dom alist1)⊃
alist∞(alist1∞alist2)=(alist∞alist1)∞alist2|)
alistinduction
(part 1(open compalist)(use alist_lemma1 * mode: always)))
;∀ALIST.MKLSET(RANGE(ALIST))⊂MKLSET(DOM(ALIST1))⊃
; ALIST∞(ALIST1∞ALIST2)=(ALIST∞ALIST1)∞ALIST2
;samemap left
(wipe-out)
(get-proofs assoc)
(proof samemap_left)
1. (assume |samemap(alist1,alist2)|)
(label sml1)
2. (rw * (open samemap))
;MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))∧
;(∀Y.YεMKLSET(DOM(ALIST1))⊃APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2))
(label sml2)
3. (assume |yεmklset dom(alist1)|)
(label sml3)
4. (derive |appalist(y,alist1)=appalist(y,alist2)| (sml2 sml3))
(label sml4)
5. (rw sml3 (use sml2 mode: exact))
;YεMKLSET(DOM(ALIST2))
(label sml5)
6. (rw sml3 (open epsilon mklset))
;MEMBER(Y,DOM(ALIST1))
7. (rw sml5 (open epsilon mklset))
;MEMBER(Y,DOM(ALIST2))
8. (trw |appalist(y,alist1∞alist)=appalist(y,alist2∞alist)|
(use app_compalist -2 mode: exact)
(use app_compalist * mode: exact)
(use sml4 mode: exact))
;APPALIST(Y,ALIST1∞ALIST)=APPALIST(Y,ALIST2∞ALIST)
;deps: (SML1 SML3)
9. (ci sml3)
;YεMKLSET(DOM(ALIST1))⊃APPALIST(Y,ALIST1∞ALIST)=APPALIST(Y,ALIST2∞ALIST)
10. (trw |mklset(dom(alist1∞alist))=mklset(dom(alist2∞alist))|
dom_compalist (use sml2 mode: exact))
;MKLSET(DOM(ALIST1∞ALIST))=MKLSET(DOM(ALIST2∞ALIST))
11. (trw |samemap(alist1∞alist,alist2∞alist)| (open samemap)
(dom_compalist * -2))
;SAMEMAP(ALIST1∞ALIST,ALIST2∞ALIST)
;deps: (SML1)
12. (ci sml1)
;SAMEMAP(ALIST1,ALIST2)⊃SAMEMAP(ALIST1∞ALIST,ALIST2∞ALIST)
;theorem 2 (i) (permutp idalistp)
(wipe-out)
(get-proofs assoc)
(proof idalistprop)
1. (ue (chi |λalist.idalistp(alist)⊃dom alist=range alist|) alistinduction
(open idalistp dom range))
;∀ALIST.IDALISTP(ALIST)⊃DOM(ALIST)=RANGE(ALIST)
2. (trw |∀alist.functp(alist)∧idalistp(alist)⊃permutp(alist)|
(open functp permutp)(use * mode: always))
;∀ALIST.FUNCTP(ALIST)∧IDALISTP(ALIST)⊃PERMUTP(ALIST)
;theorem 2 (ii) (idalistp right)
3. (assume |idalistp(alist1)|)
4. (ue (chi |λalist.mklset(range(alist))⊂mklset(dom(alist1))⊃
(alist∞alist1=alist)|)
alistinduction
(part 1(open compalist))
(use helpinduction idalistp_main * mode: always))
;∀ALIST.MKLSET(RANGE(ALIST))⊂MKLSET(DOM(ALIST1))⊃ALIST∞ALIST1=ALIST
;deps: (4)
5. (ci -2)
;IDALISTP(ALIST1)⊃
;(∀ALIST.MKLSET(RANGE(ALIST))⊂MKLSET(DOM(ALIST1))⊃ALIST∞ALIST1=ALIST)
;theorem 2 (iii) (idalistp left)
(wipe-out)
(get-proofs assoc)
(proof idalistp_left)
1. (assume |idalistp alistid|)
(label idal_l1)
;ALISTID is unknown.
;the symbol ALISTID is given the same declaration as ALIST
2. (assume |mklset dom(alistid)=mklset dom(alist)|)
(label idal_l2)
3. (assume |yεmklset(dom(alistid∞alist))|)
(label idal_l3)
4. (rw * (use alist_lemma2 mode: exact)(open epsilon mklset))
(label idal_l4)
;MEMBER(Y,DOM(ALISTID))
;deps: (idal_l3)
5. (trw |appalist(y,alistid∞alist)| (use alist_lemma1 * mode: exact))
;APPALIST(Y,ALISTID∞ALIST)=APPALIST(APPALIST(Y,ALISTID),ALIST)
(label idal_l5)
;labels: IDALISTP_MAIN
; (AXIOM
; |∀ALIST Y.IDALISTP(ALIST)∧MEMBER(Y,DOM(ALIST))⊃APPALIST(Y,ALIST)=Y|)
6. (derive |appalist(y,alistid)=y| (idalistp_main idal_l1 idal_l4))
;deps: (idal_l1 idal_l3)
7. (rw idal_l5 *)
;APPALIST(Y,ALISTID∞ALIST)=APPALIST(Y,ALIST)
;deps: (idal_l1 idal_l3)
8. (ci idal_l3)
;YεMKLSET(DOM(ALISTID∞ALIST))⊃APPALIST(Y,ALISTID∞ALIST)=APPALIST(Y,ALIST)
(label idal_l6)
;deps: (idal_l1)
9. (trw |mklset(dom(alistid∞alist))=mklset dom(alist)|
(use alist_lemma2 idal_l2 mode: exact))
;MKLSET(DOM(ALISTID∞ALIST))=MKLSET(DOM(ALIST))
;deps: (idal_l2)
;labels: SAMEMAPDEF
; (DEFINE SAMEMAP
; |∀ALIST ALIST1.SAMEMAP(ALIST,ALIST1)≡
; MKLSET(DOM(ALIST))=MKLSET(DOM(ALIST1))∧
; (∀Y.YεMKLSET(DOM(ALIST))⊃
; APPALIST(Y,ALIST)=APPALIST(Y,ALIST1))| NIL)
10. (trw |samemap(alistid∞alist,alist)| (open samemap) (idal_l6 *))
;SAMEMAP(ALISTID∞ALIST,ALIST)
;deps: (idal_l1 idal_l2)
11. (ci (idal_l1 idal_l2))
;IDALISTP(ALISTID)∧MKLSET(DOM(ALISTID))=MKLSET(DOM(ALIST))⊃
;SAMEMAP(ALISTID∞ALIST,ALIST)
;a lemma: the range of a permutation contains only atoms
(wipe-out)
(get-proofs assoc)
(proof atomrange)
1. (assume |mklset(dom(alist))=mklset(range(alist))|)
(label ar1)
2. (ue (chi |λalist.allp(λx.atom(x),dom alist)|)
alistinduction
(open allp dom))
;∀ALIST.ALLP(λX.ATOM X,DOM(ALIST))
(label ar2)
3. (ue ((phi1.|λx.atom(x)|)(x.x)(u.|dom alist|)) allp_elimination *)
;MEMBER(X,DOM(ALIST))⊃ATOM X
4. (trw |mklset dom(alist)⊂(λx.atom x)| * (open inclusion mklset) )
;MKLSET(DOM(ALIST))⊂(λX.ATOM X)
5. (rw * (use ar1 mode: exact))
;MKLSET(RANGE(ALIST))⊂(λX.ATOM X)
6. (rw * (open inclusion mklset))
;∀XV.MEMBER(XV,RANGE(ALIST))⊃ATOM XV
7. (ue ((phi1.|λx.atom x|)(u.|range alist|))
allp_introduction *)
;ALLP(λX.ATOM X,RANGE(ALIST))
8. (ci ar1)
;MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))⊃ALLP(λX.ATOM X,RANGE(ALIST))
(label atomrange)
;theorem 3 (i)
(wipe-out)
(get-proofs assoc)
(proof permutp_invalist)
;we borrow this result from the proof permutp_injectp
0. (axiom |∀alist.permutp alist⊃injectp alist|)
(label permutp_injectp)
(proof permutp_invalist)
1. (assume |permutp alist|)
(label piv1)
2. (derive |injectp alist|(permutp_injectp piv1))
;deps: (PIV1)
3. (rw * (open injectp))
;FUNCTP(ALIST)∧UNIQUENESS(RANGE(ALIST))
(label piv2)
4. (rw piv1 (open permutp))
;FUNCTP(ALIST)∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))
(label piv3)
5. (derive |allp(λx.atom x,range alist)| (atomrange *))
(label piv4)
6. (derive |dom invalist(alist)=range alist| (dom_invalist *))
(label piv5)
7. (derive |range invalist(alist)=dom alist| (range_invalist piv4))
(label piv6)
8. (trw |uniqueness dom(invalist(alist))| piv2 (use piv5))
;UNIQUENESS(DOM(INVALIST(ALIST)))
(label piv7)
9. (trw |mklset dom(invalist(alist))=mklset range(invalist(alist))|
piv3 (use piv5 piv6))
;MKLSET(DOM(INVALIST(ALIST)))=MKLSET(RANGE(INVALIST(ALIST)))
(label piv8)
10. (trw |permutp invalist(alist)| piv7 piv8
(open permutp functp) (use invalistsort piv4 mode: exact))
;PERMUTP(INVALIST(ALIST))
;deps: (PIV1)
11. (ci piv1)
;PERMUTP(ALIST)⊃PERMUTP(INVALIST(ALIST))
(label permutp_invalist)
;theorem 3 (ii) and (iii)
(wipe-out)
(get-proofs assoc)
(proof invalistprop)
1. (ue (chi |λALIST.ALLP(λX.ATOM X,RANGE(ALIST))∧INJECTP(ALIST)⊃
IDALISTP(ALIST∞INVALIST(ALIST))|) alistinduction
(part 1(use allpfact ue: ((phi.|λx.atom x|)(x.y)(u.|range alist|)) )
(open range injectp functp uniqueness invalist
idalistp compalist appalist assoc)
(use invalistsort dom_invalist compalist_lemma mode: exact)))
;∀ALIST.ALLP(λX.ATOM X,RANGE(ALIST))∧INJECTP(ALIST)⊃
; IDALISTP(ALIST∞INVALIST(ALIST))
;theorem 3 (ii)
2. (assume |ALLP(λX.ATOM X,RANGE(ALIST))|)
3. (ue ((alist.|invalist(alist)|)(alist1.|alist|)(za.xa)(z.y)) compalist_lemma
(use * invalistsort range_invalist mode: exact))
;¬MEMBER(XA,DOM(ALIST))⊃INVALIST(ALIST)∞((XA.Y).ALIST)=INVALIST(ALIST)∞ALIST
4. (ci -2)
;ALLP(λX.ATOM X,RANGE(ALIST))⊃
;(¬MEMBER(XA,DOM(ALIST))⊃INVALIST(ALIST)∞((XA.Y).ALIST)=INVALIST(ALIST)∞ALIST)
5. (ue (chi |λALIST.ALLP(λX.ATOM X,RANGE(ALIST))∧INJECTP(ALIST)⊃
IDALISTP(INVALIST(ALIST)∞ALIST)|) alistinduction
(part 1 (open allp range injectp functp uniqueness
invalist compalist appalist assoc idalistp)
invalistsort (use range_invalist mode: exact) (use * mode: always)))
;∀ALIST.ALLP(λX.ATOM X,RANGE(ALIST))∧INJECTP(ALIST)⊃
; IDALISTP(INVALIST(ALIST)∞ALIST)